Nuprl Lemma : atom2-deq_wf
0,22
postcript
pdf
Atom2Deq
EqDecider(Atom2)
latex
Definitions
Atom2Deq
,
EqDecider(
T
)
,
Atom$n
,
s
=
t
,
b
,
P
Q
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
<
a
,
b
>
,
t
T
,
Type
,
eq_atom$n(
x
;
y
)
,
x
.
A
(
x
)
,
atom2-deq-aux
,
Prop
,
#$n
,
,
Unit
,
left
+
right
,
,
f
(
a
)
Lemmas
iff
wf
,
assert
wf
,
atom2-deq-aux
,
eq
atom
wf2
origin
b, P 
Q, x:A
B(x), 
x:A. B(x), <a,b>, t 
T, Type, eq_atom$n(x;y), 
x.A(x), atom2-deq-aux, Prop, #$n, 
, Unit, left+right, 
, f(a)